;;;===========================================================================
;;;
;;; A proof of the trivial perturbation lemma
;;;
;;;---------------------------------------------------------------------------
;;;
;;; JHV 
;;;
;;; Start date: 03/05/10 || End date: 03/05/10
;;;
;;;===========================================================================


(in-package "ACL2")

(include-book "algebraic-data-structures")

(encapsulate
 
 ;;**************************************************
 ;; Signaturas
 ;;**************************************************

 (
 ;;--------------------------------------------------
 ;; The signatures of the ring R
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-ring *) => *)
 ;; Addition operation ring
 ((addition-ring * *)=> *)
 ;; Product operation ring
 ((product-ring * *) => *)
 ;; Inverse ring
 ((inverse *) => *)
 ;; Zero element ring
 ((zero-element ) => *)
 ;; Unit element ring
 ((unit )=> *)

 ;;--------------------------------------------------
 ;; Top Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-top * *) => *)
 ;; Group Operation 
 ((group-operation-top * * *) => *)
 ;; Zero element
 ((zero-top *) => *)
 ;; External multiplication
 ((external-top * * *) => *)
 ;; Inverse element
 ((inverse-top * *) => *)

 ;;--------------------------------------------------
 ;; The top differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-top * *) => *)
 


 ;;--------------------------------------------------
 ;; Bottom Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-bottom * *) => *)
 ;; Group Operation 
 ((group-operation-bottom * * *) => *)
 ;; Zero element
 ((zero-bottom *) => *)
 ;; External multiplication
 ((external-bottom * * *) => *)
 ;; Inverse element
 ((inverse-bottom * *) => *)

 ;;--------------------------------------------------
 ;; The bottom differential
 ;;--------------------------------------------------

 ;; The differential
 ((d-bottom * *) => *)
 

 ;;--------------------------------------------------
 ;; The f morphism
 ;;--------------------------------------------------

 ;; The function
 ((f * *) => *)
 

 ;;--------------------------------------------------
 ;; The g morphism
 ;;--------------------------------------------------

 ;; The function
 ((g * *) => *)
 


 ;;--------------------------------------------------
 ;; The h morphism
 ;;--------------------------------------------------

 ;; The function
 ((h * *) => *)
 


 ;;--------------------------------------------------
 ;; The perturbation
 ;;--------------------------------------------------

 ;; The function
 ((delta * *) => *)
 

 
 )
 ;;**************************************************
 ;; Witnesses
 ;;**************************************************
 
 ;;--------------------------------------------------
 ;; The witnesses of the ring Z
 ;;--------------------------------------------------

 ;; The characteristic function

 (local (defun inv-ring (a)
	  (integerp a)))
 
 ;; Addition operation Z
 (local (defun addition-ring (a b)
	  (+ a b)))

 ;; Product operation ring
 (local (defun product-ring (a b)
	  (* a b)))

 ;; Inverse addition
 (local (defun inverse (a)
	  (- a)))

 ;; Zero element ring
 (local (defun zero-element nil
	  0))

 ;; Unit element ring
 (local (defun unit nil
	  1))

 ;;--------------------------------------------------
 ;; Top Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-top (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-top (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-top (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-top (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-top (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The top differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-top (n a)
	  (declare (ignore n a))
	  0))

 

 ;;--------------------------------------------------
 ;; Bottom Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-bottom (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-bottom (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-bottom (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-bottom (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse bottom
 (local (defun inverse-bottom (n a)
	  (declare (ignore n a))
	  0))

 


 ;;--------------------------------------------------
 ;; The bottom differential
 ;;--------------------------------------------------
 
  ;; The differential
 (local (defun d-bottom (n a)
	  (declare (ignore n a))
	  0))

 

 
 

 ;;--------------------------------------------------
 ;; The f morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun f (n a)
	  (declare (ignore n a))
	  0))




 ;;--------------------------------------------------
 ;; The g morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun g (n a)
	  (declare (ignore n a))
	  0))


 

 ;;--------------------------------------------------
 ;; The h morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun h (n a)
	  (declare (ignore n a))
	  0))




 ;;--------------------------------------------------
 ;; The perturbation
 ;;--------------------------------------------------

 ;; The function
 (local (defun delta (n a)
	  (declare (ignore n a))
	  0))


   
 (defun perturbation (n gnrt)
   (group-operation-bottom (1- n) (d-bottom n gnrt) (delta n gnrt)))



  ;;************************************************** 
  ;; Properties
  ;;************************************************** 
  

(check-reduction-p
(reduction 
 (chain-complex 
   'inv-ring 'addition-ring 'zero-element 'inverse 'product-ring 'unit 
   'inv-top 'group-operation-top 'zero-top 'external-top 'inverse-top 'd-top )
  (chain-complex 
    'inv-ring 'addition-ring 'zero-element 'inverse 'product-ring 'unit
    'inv-bottom 'group-operation-bottom 'zero-bottom 'external-bottom 'inverse-bottom 'd-bottom )
  'f  'g  'h
   ) 'reduction)

 

 ;;--------------------------------------------------
 ;; Properties of the delta
 ;;--------------------------------------------------

  ;; The delta is a morphism
(check-morphism-degree--1-p
(morphism-degree--1 'inv-bottom 'inv-bottom 'delta 'group-operation-bottom 'group-operation-bottom 'external-bottom  'external-bottom 'inv-ring				      
		    'zero-bottom 'zero-bottom 'inverse-bottom 'inverse-bottom)
'delta
)

 ;;--------------------------------------------------
 ;; Properties of the perturbation
 ;;--------------------------------------------------

 ;; The perturbation is a differential
(check-differential-p
(differential 'inv-bottom 'perturbation 'group-operation-bottom 'external-bottom 'inv-ring 'zero-bottom  'inverse-bottom)
'perturbation
)
)


;;==================================================
;; The new definitions
;;==================================================


 ;;--------------------------------------------------
 ;; New Top Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
(defun new-inv-top (n a) 
   (inv-top n a))

 ;; Group Operation 
(defun new-group-operation-top (n a b)
	  (group-operation-top n a b))

 ;; Zero element
(defun new-zero-top (n)
   (zero-top n))

 ;; External multiplication
(defun new-external-top (n a b)
	 (external-top n a b))

 ;; Inverse element
(defun new-inverse-top (n a)
   (inverse-top n a))
	 

 ;;--------------------------------------------------
 ;; The new top differential 
 ;;--------------------------------------------------

 ;; The differential
(defun new-d-top (n a)
  (group-operation-top (1- n) (d-top n a) (g (1- n)(delta n (f n a))))
	  )




 ;;--------------------------------------------------
 ;; New Bottom Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
(defun new-inv-bottom (n a) 
   (inv-bottom n a))
	  

 ;; Group Operation 
(defun new-group-operation-bottom (n a b)
	  (group-operation-bottom n a b))
	  

 ;; Zero element
(defun new-zero-bottom (n)
  (zero-bottom n))
	  

 ;; External multiplication
(defun new-external-bottom (n a b)
   (external-bottom n a b))


 ;; Inverse bottom
(defun new-inverse-bottom (n a)
  (inverse-bottom n a))
 


 ;;--------------------------------------------------
 ;; The new bottom differential
 ;;--------------------------------------------------
 
  ;; The differential
(defun new-d-bottom (n a)
   (perturbation n a))


	  

 ;;--------------------------------------------------
 ;; The new f morphism
 ;;--------------------------------------------------

 ;; The function
(defun new-f (n a)
   (f n a))


	  


 ;;--------------------------------------------------
 ;; The new g morphism
 ;;--------------------------------------------------

 ;; The function
(defun new-g (n a)
	  (g n a))


	  

 ;;--------------------------------------------------
 ;; The new h morphism
 ;;--------------------------------------------------

 ;; The function
(defun new-h (n a)
   (h n a))
	  


 
 

;;===========================================================================
;; The properties
;;===========================================================================



(defthm bottom-aux-prop1
  (implies (and (inv-bottom n a)
		(inv-bottom n b)
		(inv-bottom n c)
		(integerp n))
	   (equal (group-operation-bottom n (group-operation-bottom n a b) c)
		  (group-operation-bottom n a (group-operation-bottom n b c))))
  :hints (("Goal" :use ((:instance |REDUCTION-is-a-reduction|)))))


(defthm top-aux-prop1
  (implies (and (inv-top n a)
		(inv-top n b)
		(inv-top n c)
		(integerp n))
	   (equal (group-operation-top n (group-operation-top n a b) c)
		  (group-operation-top n a (group-operation-top n b c))))
  :hints (("Goal" :use ((:instance |REDUCTION-is-a-reduction|)))))


(encapsulate 
 
 ()

 (defthm subgoal38-help-1
   (implies (and (inv-top (+ -1 n) a)
		 (inv-top (+ -1 n) b) (integerp n))
	    (inv-top (+ -1 n) (group-operation-top (+ -1 n) a b))))

 (defthm subgoal38-help-2
   (implies (and (inv-top n a) (integerp n))
	    (inv-top (+ n -1) (d-top n a)))
  :hints (("Goal" :use ((:instance |REDUCTION-is-a-reduction|))))) 

(defthm subgoal38-help-2-bis
   (implies (and (inv-top n a) (integerp n))
	    (inv-top (+ -1 n) (d-top n a)))
  :hints (("Goal" :use ((:instance subgoal38-help-2)))))


 (defthm subgoal38-help-3
   (implies (and (inv-top n a) (integerp n))
	    (inv-bottom n (f n a)))
  :hints (("Goal" :use ((:instance |REDUCTION-is-a-reduction|)))))


 (defthm subgoal38-help-4
   (implies (and (inv-bottom n a) (integerp n))
	    (inv-bottom (+ -1 n) (delta n a)))
  :hints (("Goal" :use ((:instance |DELTA-is-a-morphism-of-degree--1|)))))
 
 (defthm subgoal38-help-5
   (implies (and (inv-bottom n a) (integerp n))
	    (inv-top  n (g n a)))
  :hints (("Goal" :use ((:instance |REDUCTION-is-a-reduction|)))))

 (defthm subgoal38-help-6
   (implies (and (inv-bottom (+ -1 n) a) (integerp n))
	    (inv-top (+ -1 n)  (g (+ -1 n) a)))
  :hints (("Goal" :use ((:instance subgoal38-help-5
				   (n (+ -1 n)))))))

 (defthm subgoal38-help
   (implies (and (inv-top n a) (integerp n))
	    (inv-top (+ -1 n)  (g (+ -1 n) (delta n (f n a)))))
  :hints (("Goal" :use ((:instance subgoal38-help-3)
			(:instance subgoal38-help-4)
			(:instance subgoal38-help-6)))))
)

(encapsulate 

 ()

 (local (defthm subgoal37-help-1
   (implies (and (inv-top (+ -1 n) a)
		 (inv-top (+ -1 n) b)
		 (inv-top (+ -1 n) c)
		 (integerp n))
	    (equal (group-operation-top (+ -1 n) a (group-operation-top (+ -1 n) b c))
		   (group-operation-top (+ -1 n) a (group-operation-top (+ -1 n) c b))))
   ))

 (local (defthm subgoal37-help-2
   (implies (and (inv-top (+ -1 n) a)
		 (inv-top (+ -1 n) b)
		 (inv-top (+ -1 n) c)
		 (integerp n))
	    (equal (group-operation-top (+ -1 n) a (group-operation-top (+ -1 n) c b))
		   (group-operation-top (+ -1 n) (group-operation-top (+ -1 n) a c) b)))
   ))

 (local (defthm subgoal37-help-3
   (implies (and (inv-top (+ -1 n) a)
		 (inv-top (+ -1 n) b)
		 (integerp n))
	    (equal (group-operation-top (+ -1 n) a b)
		   (group-operation-top (+ -1 n) b a)))
   ))

 (local (defthm subgoal37-help-4
   (implies (and (inv-top (+ -1 n) a)
		 (inv-top (+ -1 n) b)
		 (inv-top (+ -1 n) c)
		 (integerp n))
	    (equal (group-operation-top (+ -1 n) (group-operation-top (+ -1 n) a c) b)
		   (group-operation-top (+ -1 n) b (group-operation-top (+ -1 n) a c))))
   :hints (("Goal" :in-theory (disable subgoal37-help-2)
	    :use ((:instance subgoal37-help-3 (a (group-operation-top (+ -1 n) a c)))))))
	)
 
 (local (defthm subgoal37-help-5
   (implies (and (inv-top (+ -1 n) a)
		 (inv-top (+ -1 n) b)
		 (inv-top (+ -1 n) c)
		 (integerp n))
	    (equal (group-operation-top (+ -1 n) a (group-operation-top (+ -1 n) b c))
		   (group-operation-top (+ -1 n) b (group-operation-top (+ -1 n) a c))))
   :hints (("Goal" :in-theory (disable subgoal37-help-2)
	    :use ((:instance subgoal37-help-1)
		  (:instance subgoal37-help-2)
		  (:instance subgoal37-help-4))))))

  (defthm subgoal37-help
   (implies (and (inv-top n a)
		 (inv-top n b)
		 (integerp n))
	    (equal (group-operation-top
                     (+ -1 n)
                     (d-top n b)
                     (group-operation-top (+ -1 n)
                                          (g (+ -1 n) (delta n (f n a)))
                                          (g (+ -1 n) (delta n (f n b)))))
		  (group-operation-top
                     (+ -1 n)
                     (g (+ -1 n) (delta n (f n a)))
                     (group-operation-top (+ -1 n)
                                          (d-top n b)
                                          (g (+ -1 n) (delta n (f n b))))) )
	    )
   :hints (("Goal" :in-theory (disable subgoal37-help-2)
	    )))

)



(encapsulate 
 
 ()


(defthm closure-d-bottom
   (implies (and (inv-bottom n a) (integerp n))
	    (inv-bottom (+ n -1) (d-bottom n a)))
  :hints (("Goal" :use ((:instance |REDUCTION-is-a-reduction|)))))

(defthm closure-d-bottom-2
   (implies (and (inv-bottom n a) (integerp n))
	    (inv-bottom (+ -1 n) (d-bottom n a)))
  :hints (("Goal" :use ((:instance closure-d-bottom)))))

(defthm closure-g-d-bottom-delta-f
  (implies (and (inv-top n a) (integerp n))
	   (inv-top (1- (1- n)) (g (1- (1- n)) 
				   (d-bottom (1- n) (delta n (f n a)))))))

(defthm closure-g-delta-delta-f
  (implies (and (inv-top n a) (integerp n))
	   (inv-top (1- (1- n)) (g (1- (1- n)) 
				   (delta (1- n) (delta n (f n a)))))))

(defthm closure-g-delta-f-d-top
  (implies (and (inv-top n a) (integerp n))
	   (inv-top (1- (1- n)) (g (1- (1- n)) 
				   (delta (1- n) (f (1- n) (d-top n a)))))))

(defthm closure-delta-delta-f
  (implies (and (inv-top n a) (integerp n))
	   (inv-bottom (1- (1- n)) (delta (1- n) (delta n (f n a))))))

(defthm closure-delta-f-d-top
  (implies (and (inv-top n a) (integerp n))
	   (inv-bottom (1- (1- n)) (delta (1- n) (f (1- n) (d-top n a))))))



(defthm closure-d-bottom-delta
  (implies (and (inv-bottom n a) (integerp n))
	   (inv-bottom (1- (1- n)) (d-bottom (1- n) (delta n a)))))

(defthm closure-delta-delta
  (implies (and (inv-bottom n a) (integerp n))
	   (inv-bottom (1- (1- n)) (delta (1- n) (delta n a)))))

(defthm closure-delta-d-bottom
  (implies (and (inv-bottom n a) (integerp n))
	   (inv-bottom (1- (1- n)) (delta (1- n) (d-bottom n a)))))


)


(defthm perturbationoperturbation
  (implies (and (inv-bottom n a) (integerp n))
         (equal (perturbation (+ -1 n)
                              (perturbation n a))
                (zero-bottom (+ -1 -1 n))))
  :hints (("Goal" :in-theory (disable perturbation))))


(defthm closure-h
  (implies (and (inv-top n a) (integerp n))
	   (inv-top (+ n 1) (h n a)))
  :hints (("Goal" :use ((:instance |REDUCTION-is-a-reduction|)))))

(defthm closure-h-2
  (implies (and (inv-top n a) (integerp n))
	   (inv-top (+ 1 n) (h n a)))
  :hints (("Goal" :use ((:instance closure-h)))))


(encapsulate

  ()

 (local (defthm 1-1+n
   (implies (integerp n)
	    (equal (+ -1 1 n) n))))
(local 
 (defthm 1-1+n2
   (implies (integerp n)
	    (equal (1- (1+ n)) n))))

 (local (defthm 1+1-n2
   (implies (integerp n)
	    (equal (1+ (1- n)) n))))

 (local (defthm new-hod+doh-aux
   (implies (and  (new-inv-top n a) (integerp n))
	    (equal (group-operation-top (+ -1 1 n) a (zero-top (+ -1 1 n)))
		   a))))

 (local (defthm inv-d-top-h
   (implies (and (inv-top n a) (integerp n))
	    (inv-top (1- (1+ n)) (d-top (+ 1 n) (h n a))))
   :hints (("Goal" :in-theory (disable 1-1+n2 1+1-n2 1-1+n)))))

(local (defthm inv-d-top-h2
   (implies (and (inv-top n a) (integerp n))
	    (inv-top n (d-top (+ 1 n) (h n a))))
   :hints (("Goal" :use ((:instance inv-d-top-h)
			 (:instance 1-1+n2))))
   ))

(local (defthm inv-h-d-top
   (implies (and (inv-top n a) (integerp n))
	    (inv-top (1+ (1- n)) (h (1- n) (d-top n a))))
   :hints (("Goal" :in-theory (disable 1-1+n2 1+1-n2 1-1+n)))))

(local (defthm inv-h-d-top-2
   (implies (and (inv-top n a) (integerp n))
	    (inv-top n (h (1- n) (d-top n a))))
   :hints (("Goal" :use ((:instance inv-h-d-top)
			 (:instance 1+1-n2))))
   ))

(local (defthm group-operation-top-zero
	 (implies (and (inv-top n a) (integerp n))
		  (equal (group-operation-top n (zero-top n) a)
			 a))))

 (defthm new-hod+doh
   (implies (and (new-inv-top n a) (integerp n))
	    (equal (new-group-operation-top n (new-h (1- n) (new-d-top n a))
		      (new-d-top (1+ n) (new-h n a)))
		   (new-group-operation-top n a
		      (new-inverse-top n (new-g n (new-f n a))))))
   )

(defthm new-hod+doh-2
   (implies (and (inv-top n gnrt) (integerp n))
	    (equal (group-operation-top n (h (+ -1 n) (new-d-top n gnrt))
		      (new-d-top (+ 1 n) (h n gnrt)))
		   (group-operation-top n gnrt
		      (inverse-top n (g n (f n gnrt))))))
   :hints (("Goal" :use ((:instance  new-hod+doh (a gnrt))
			 ))))

)


(encapsulate 
 
 ()

(local (defthm d-d-bottom
    (implies (and (inv-bottom n a) (integerp n))
             (equal (d-bottom (1- n) (d-bottom n a))
                    (zero-bottom (1- (1- n)))))))

(local  (defthm existence-identity-element-bcc
   (implies (and (inv-bottom n a) (integerp n))
	    (equal (group-operation-bottom n a (zero-bottom n))
		   a))))

(local (defthm commutativity-bcc
    (implies (and (inv-bottom n a) (inv-bottom n b) (integerp n))
             (equal (group-operation-bottom n a b)
                    (group-operation-bottom n b a)))))

(local (DEFTHM CLOSURE-ZERO-ELEMENT-BCC
                      (INV-BOTTOM N (ZERO-BOTTOM N))))

(local (DEFTHM
	 DISTRIBUTIVITY-D-BOTTOM
                  (IMPLIES (AND (INV-BOTTOM N A) (INV-BOTTOM N B) (integerp n))
                           (EQUAL (D-BOTTOM N (GROUP-OPERATION-BOTTOM N A B))
                                  (GROUP-OPERATION-BOTTOM (1- N)
                                                          (D-BOTTOM N A)
                                                          (D-BOTTOM N B))))))

(local (DEFTHM
                   DISTRIBUTIVITY-DELTA
                   (IMPLIES (AND (INV-BOTTOM N A) (INV-BOTTOM N B) (integerp n))
                            (EQUAL (DELTA N (GROUP-OPERATION-BOTTOM N A B))
                                   (GROUP-OPERATION-BOTTOM (1- N)
                                                           (DELTA N A)
                                                           (DELTA N B))))))
(local (defthm ddelta+deltadelta+deltad2
  (implies (and (new-inv-bottom n a)  (integerp n))
	   (equal (group-operation-bottom  (+ -1 -1 n)
					   (d-bottom (1- n) (delta n a))
					   (group-operation-bottom (+ -1 -1 n)
								   (delta (1- n) (delta n a))
								   (delta (1- n) (d-bottom n a))))
		 (new-d-bottom (1- n) (new-d-bottom n a))
		  ))
  :hints (("Goal" :in-theory (disable |REDUCTION-is-a-reduction|
				      |PERTURBATION-is-a-differential|)
	   :use ((:instance existence-identity-element-bcc
					    (a (d-bottom (1- n) (delta n a)))
					    (n (1- (1- n)) )))))))
		   
(local(defthm ddelta+deltadelta+deltad
  (implies (and (new-inv-bottom n a) (integerp n))
	   (equal (group-operation-bottom  (+ -1 -1 n)
					   (d-bottom (1- n) (delta n a))
					   (group-operation-bottom (+ -1 -1 n)
								   (delta (1- n) (delta n a))
								   (delta (1- n) (d-bottom n a))))
		 (new-zero-bottom (+ -1 -1 n))
		  ))
  :hints (("Goal" :in-theory  (disable perturbation)
	   :use ((:instance ddelta+deltadelta+deltad2))
	   ))))


(local(defthm new-d-d-top-aux1
  (implies (and (inv-top n a) (integerp n))
	   (equal (group-operation-top
		   (+ -1 -1 n)
		   (g (+ -1 -1 n)
		      (d-bottom (+ -1 n) (delta n (f n a))))
		   (group-operation-top (+ -1 -1 n)
					(g (+ -1 -1 n)
					   (delta (+ -1 n) (delta n (f n a))))
					(g (+ -1 -1 n)
					   (delta (+ -1 n)
						  (f (+ -1 n) (d-top n a))))))
		  (group-operation-top
		   (+ -1 -1 n)
		   (g (+ -1 -1 n)
		      (d-bottom (+ -1 n) (delta n (f n a))))
		   (g (+ -1 -1 n) (group-operation-bottom (+ -1 -1 n)
						       (delta (+ -1 n) (delta n (f n a)))
						       (delta (+ -1 n) (f (+ -1 n) (d-top n a))))
					)))
  )))

(local(defthm new-d-d-top-aux2
  (implies (and (inv-top n a) (integerp n))
	   (equal (group-operation-top
		   (+ -1 -1 n)
		   (g (+ -1 -1 n)
		      (d-bottom (+ -1 n) (delta n (f n a))))
		   (group-operation-top (+ -1 -1 n)
					(g (+ -1 -1 n)
					   (delta (+ -1 n) (delta n (f n a))))
					(g (+ -1 -1 n)
					   (delta (+ -1 n)
						  (f (+ -1 n) (d-top n a))))))
		  (g (+ -1 -1 n)
		     (group-operation-bottom
		      (+ -1 -1 n)
		      (d-bottom (+ -1 n) (delta n (f n a)))
		    (group-operation-bottom (+ -1 -1 n)
						       (delta (+ -1 n) (delta n (f n a)))
						       (delta (+ -1 n) (f (+ -1 n) (d-top n a))))
					))
  ))
  :hints (("Goal" :in-theory (disable new-d-d-top-aux1)))))

(local(defthm new-d-d-top-aux3
  (implies (and (inv-top n a) (integerp n))
	   (equal (group-operation-top
		   (+ -1 -1 n)
		   (g (+ -1 -1 n)
		      (d-bottom (+ -1 n) (delta n (f n a))))
		   (group-operation-top (+ -1 -1 n)
					(g (+ -1 -1 n)
					   (delta (+ -1 n) (delta n (f n a))))
					(g (+ -1 -1 n)
					   (delta (+ -1 n)
						  (f (+ -1 n) (d-top n a))))))
		  (g (+ -1 -1 n)
		     (group-operation-bottom
		      (+ -1 -1 n)
		      (d-bottom (+ -1 n) (delta n (f n a)))
		    (group-operation-bottom (+ -1 -1 n)
						       (delta (+ -1 n) (delta n (f n a)))
						       (delta (+ -1 n) (d-bottom n (f n a))))
					))
  ))
  :hints (("Goal" :in-theory (disable new-d-d-top-aux1 new-d-d-top-aux2)))))

(local(defthm ddelta+deltadelta+deltad-bis
  (implies (and (inv-bottom n a) (integerp n))
	   (equal (group-operation-bottom  (+ -1 -1 n)
					   (d-bottom (1- n) (delta n a))
					   (group-operation-bottom (+ -1 -1 n)
								   (delta (1- n) (delta n a))
								   (delta (1- n) (d-bottom n a))))
		 (new-zero-bottom (+ -1 -1 n))
		  ))
  :hints (("Goal"  
	   :use ((:instance ddelta+deltadelta+deltad))
	   ))))

(local(defthm new-d-d-top-aux4
  (implies (and (inv-top n a)  (integerp n))
	   (equal (group-operation-top
		   (+ -1 -1 n)
		   (g (+ -1 -1 n)
		      (d-bottom (+ -1 n) (delta n (f n a))))
		   (group-operation-top (+ -1 -1 n)
					(g (+ -1 -1 n)
					   (delta (+ -1 n) (delta n (f n a))))
					(g (+ -1 -1 n)
					   (delta (+ -1 n)
						  (f (+ -1 n) (d-top n a))))))
		  (g (+ -1 -1 n) (new-zero-bottom (+ -1 -1 n)))))
  :hints (("Goal" :in-theory (disable new-d-d-top-aux1 new-d-d-top-aux2 |REDUCTION-is-a-reduction|
				      |PERTURBATION-is-a-differential|
				      commutativity-bcc)))))

(local(defthm new-d-d-top-aux5
  (implies (and (inv-top n a) (integerp n))
	   (equal (group-operation-top
		   (+ -1 -1 n)
		   (g (+ -1 -1 n)
		      (d-bottom (+ -1 n) (delta n (f n a))))
		   (group-operation-top (+ -1 -1 n)
					(g (+ -1 -1 n)
					   (delta (+ -1 n) (delta n (f n a))))
					(g (+ -1 -1 n)
					   (delta (+ -1 n)
						  (f (+ -1 n) (d-top n a))))))
		  (g (+ -1 -1 n) (zero-bottom (+ -1 -1 n)))))
  :hints (("Goal" :in-theory (disable new-d-d-top-aux1 new-d-d-top-aux2 |REDUCTION-is-a-reduction|
				      |PERTURBATION-is-a-differential| 
				      commutativity-bcc)))))

(local (defthm g-zero
	 (implies (integerp n)
		  (equal (g n (zero-bottom n))
			 (zero-top n)))))


(local (defthm g-zero-2
	  (implies (integerp n)
	 (equal (g (+ -1 -1 n) (zero-bottom (+ -1 -1 n)))
		(zero-top (+ -1 -1 n))))))

(local(defthm new-d-d-top-aux
  (implies (and (inv-top n a) (integerp n))
	   (equal (group-operation-top
		   (+ -1 -1 n)
		   (g (+ -1 -1 n)
		      (d-bottom (+ -1 n) (delta n (f n a))))
		   (group-operation-top (+ -1 -1 n)
					(g (+ -1 -1 n)
					   (delta (+ -1 n) (delta n (f n a))))
					(g (+ -1 -1 n)
					   (delta (+ -1 n)
						  (f (+ -1 n) (d-top n a))))))
		  (zero-top (+ -1 -1 n))))
  :hints (("Goal" :in-theory (disable new-d-d-top-aux1 new-d-d-top-aux2
				      |REDUCTION-is-a-reduction|
				      |PERTURBATION-is-a-differential| 
				      commutativity-bcc)))))


 (local (defthm new-d-d-top-1
   (implies (and (new-inv-top n a)  (integerp n))
	    (equal (new-d-top (1- n) (new-d-top n a)) 
		   (new-zero-top (1- (1- n)))))
   ))

(defthm new-d-d-top
   (implies (and (inv-top n a)  (integerp n))
	    (equal (new-d-top (1- n) (new-d-top n a)) 
		   (zero-top (+ -1 -1 N))))
   )
)


(defthm group-operation-zero
  (implies (and (inv-top n gnrt)
		(integerp n))
	   (equal (group-operation-top n
				       (zero-top n)
				       gnrt)
		  gnrt)))

	   


(check-reduction-p
 (reduction 
 (chain-complex 
  'inv-ring 'addition-ring 'zero-element 'inverse 'product-ring 'unit 
   'new-inv-top 'new-group-operation-top 'new-zero-top 'new-external-top 'new-inverse-top 'new-d-top )
 (chain-complex 
   'inv-ring 'addition-ring 'zero-element 'inverse 'product-ring 'unit
    'new-inv-bottom 'new-group-operation-bottom 'new-zero-bottom 'new-external-bottom 'new-inverse-bottom 'new-d-bottom )
  'new-f  'new-g  'new-h
  ) 'perturbed-reduction
:hints '(("Subgoal 45" :use ((:instance new-d-d-top)))
	   ("Subgoal 23" :use ((:instance perturbationoperturbation)))
	   )
)


;;;===========================================================================
;;;
;;; End of the proof of the Trivial Perturbation Lemma
;;;
;;;===========================================================================



;;;----------------------------------------------------------------------------
;;; 
;;; Defining the generic theory:
;;;
;;;----------------------------------------------------------------------------


(include-book "generic-theory")


#|
(get-event-lst 
 '(perturbation
   new-inv-top
   new-group-operation-top
   new-zero-top
   new-external-top 
   new-inverse-top
   new-d-top
   new-inv-bottom 
   new-group-operation-bottom
   new-zero-bottom 
   new-external-bottom
   new-inverse-bottom
   new-d-bottom
   new-f
   new-g 
   new-h 
   |PERTURBED-REDUCTION-is-a-reduction|
   )
 )
|#


(defconst *tpl*
  '((DEFUN PERTURBATION (N GNRT)
        (GROUP-OPERATION-BOTTOM (1- N)
                                (D-BOTTOM N GNRT)
                                (DELTA N GNRT)))
 (DEFUN NEW-INV-TOP (N A) (INV-TOP N A))
 (DEFUN NEW-GROUP-OPERATION-TOP (N A B)
        (GROUP-OPERATION-TOP N A B))
 (DEFUN NEW-ZERO-TOP (N) (ZERO-TOP N))
 (DEFUN NEW-EXTERNAL-TOP (N A B)
        (EXTERNAL-TOP N A B))
 (DEFUN NEW-INVERSE-TOP (N A)
        (INVERSE-TOP N A))
 (DEFUN NEW-D-TOP (N A)
        (GROUP-OPERATION-TOP (1- N)
                             (D-TOP N A)
                             (G (1- N) (DELTA N (F N A)))))
 (DEFUN NEW-INV-BOTTOM (N A)
        (INV-BOTTOM N A))
 (DEFUN NEW-GROUP-OPERATION-BOTTOM (N A B)
        (GROUP-OPERATION-BOTTOM N A B))
 (DEFUN NEW-ZERO-BOTTOM (N)
        (ZERO-BOTTOM N))
 (DEFUN NEW-EXTERNAL-BOTTOM (N A B)
        (EXTERNAL-BOTTOM N A B))
 (DEFUN NEW-INVERSE-BOTTOM (N A)
        (INVERSE-BOTTOM N A))
 (DEFUN NEW-D-BOTTOM (N A)
        (PERTURBATION N A))
 (DEFUN NEW-F (N A) (F N A))
 (DEFUN NEW-G (N A) (G N A))
 (DEFUN NEW-H (N A) (H N A))
 (DEFTHM
  |PERTURBED-REDUCTION-is-a-reduction|
  (AND
   (AND
    (AND
     (AND
      (AND
       (AND
           (AND (AND (IMPLIES (AND (INV-RING X) (INV-RING Y))
                              (INV-RING (ADDITION-RING X Y)))
                     (IMPLIES (AND (INV-RING X)
                                   (INV-RING Y)
                                   (INV-RING Z))
                              (EQUAL (ADDITION-RING (ADDITION-RING X Y) Z)
                                     (ADDITION-RING X (ADDITION-RING Y Z)))))
                (IMPLIES (INV-RING X)
                         (EQUAL (ADDITION-RING (ZERO-ELEMENT) X)
                                X))
                (IMPLIES (INV-RING X)
                         (EQUAL (ADDITION-RING X (ZERO-ELEMENT))
                                X))
                (INV-RING (ZERO-ELEMENT)))
           (IMPLIES (INV-RING X)
                    (EQUAL (ADDITION-RING (INVERSE X) X)
                           (ZERO-ELEMENT)))
           (IMPLIES (INV-RING X)
                    (EQUAL (ADDITION-RING X (INVERSE X))
                           (ZERO-ELEMENT)))
           (IMPLIES (INV-RING X)
                    (INV-RING (INVERSE X))))
       (AND (AND (IMPLIES (AND (INV-RING X) (INV-RING Y))
                          (INV-RING (PRODUCT-RING X Y)))
                 (IMPLIES (AND (INV-RING X)
                               (INV-RING Y)
                               (INV-RING Z))
                          (EQUAL (PRODUCT-RING (PRODUCT-RING X Y) Z)
                                 (PRODUCT-RING X (PRODUCT-RING Y Z)))))
            (IMPLIES (INV-RING X)
                     (EQUAL (PRODUCT-RING (UNIT) X) X))
            (IMPLIES (INV-RING X)
                     (EQUAL (PRODUCT-RING X (UNIT)) X))
            (INV-RING (UNIT)))
       (IMPLIES (AND (INV-RING X)
                     (INV-RING Y)
                     (INV-RING Z))
                (EQUAL (PRODUCT-RING X (ADDITION-RING Y Z))
                       (ADDITION-RING (PRODUCT-RING X Y)
                                      (PRODUCT-RING X Z))))
       (IMPLIES (AND (INV-RING X)
                     (INV-RING Y)
                     (INV-RING Z))
                (EQUAL (PRODUCT-RING (ADDITION-RING X Y) Z)
                       (ADDITION-RING (PRODUCT-RING X Z)
                                      (PRODUCT-RING Y Z)))))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (NEW-INV-TOP N B)
                    (INTEGERP N))
               (NEW-INV-TOP N (NEW-GROUP-OPERATION-TOP N A B)))
      (IMPLIES
       (AND (NEW-INV-TOP N A)
            (NEW-INV-TOP N B)
            (NEW-INV-TOP N C)
            (INTEGERP N))
       (EQUAL (NEW-GROUP-OPERATION-TOP N (NEW-GROUP-OPERATION-TOP N A B)
                                       C)
              (NEW-GROUP-OPERATION-TOP N A (NEW-GROUP-OPERATION-TOP N B C))))
      (NEW-INV-TOP N (NEW-ZERO-TOP N))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (INV-RING R)
                    (INTEGERP N))
               (NEW-INV-TOP N (NEW-EXTERNAL-TOP N R A)))
      (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
               (EQUAL (NEW-GROUP-OPERATION-TOP N A (NEW-ZERO-TOP N))
                      A))
      (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
               (NEW-INV-TOP N (NEW-INVERSE-TOP N A)))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (NEW-INV-TOP N B)
                    (INTEGERP N)
                    (EQUAL (NEW-GROUP-OPERATION-TOP N A B)
                           (NEW-ZERO-TOP N)))
               (EQUAL (NEW-INVERSE-TOP N A) B))
      (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
               (EQUAL (NEW-GROUP-OPERATION-TOP N A (NEW-INVERSE-TOP N A))
                      (NEW-ZERO-TOP N)))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (NEW-INV-TOP N B)
                    (INTEGERP N))
               (EQUAL (NEW-GROUP-OPERATION-TOP N A B)
                      (NEW-GROUP-OPERATION-TOP N B A)))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (NEW-INV-TOP N B)
                    (INV-RING R)
                    (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-TOP N R (NEW-GROUP-OPERATION-TOP N A B))
                      (NEW-GROUP-OPERATION-TOP N (NEW-EXTERNAL-TOP N R A)
                                               (NEW-EXTERNAL-TOP N R B))))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (INV-RING S)
                    (INV-RING R)
                    (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-TOP N (ADDITION-RING S R)
                                        A)
                      (NEW-GROUP-OPERATION-TOP N (NEW-EXTERNAL-TOP N S A)
                                               (NEW-EXTERNAL-TOP N R A))))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (INV-RING S)
                    (INV-RING R)
                    (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-TOP N (PRODUCT-RING S R)
                                        A)
                      (NEW-EXTERNAL-TOP N S (NEW-EXTERNAL-TOP N R A))))
      (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-TOP N (UNIT) A) A))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (NEW-INV-TOP N B)
                    (INTEGERP N))
               (EQUAL (NEW-INVERSE-TOP N (NEW-GROUP-OPERATION-TOP N A B))
                      (NEW-GROUP-OPERATION-TOP N (NEW-INVERSE-TOP N A)
                                               (NEW-INVERSE-TOP N B))))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (INV-RING S)
                    (INTEGERP N))
               (EQUAL (NEW-INVERSE-TOP N (NEW-EXTERNAL-TOP N S A))
                      (NEW-EXTERNAL-TOP N S (NEW-INVERSE-TOP N A))))
      (IMPLIES (INTEGERP N)
               (EQUAL (NEW-INVERSE-TOP N (NEW-ZERO-TOP N))
                      (NEW-ZERO-TOP N)))
      (IMPLIES (AND (INV-RING S) (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-TOP N S (NEW-ZERO-TOP N))
                      (NEW-ZERO-TOP N))))
     (AND (AND (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
                        (NEW-INV-TOP (+ N -1) (NEW-D-TOP N A)))
               (IMPLIES (AND (NEW-INV-TOP N A)
                             (NEW-INV-TOP N B)
                             (INTEGERP N))
                        (EQUAL (NEW-D-TOP N (NEW-GROUP-OPERATION-TOP N A B))
                               (NEW-GROUP-OPERATION-TOP (+ N -1)
                                                        (NEW-D-TOP N A)
                                                        (NEW-D-TOP N B))))
               (IMPLIES (AND (NEW-INV-TOP N A)
                             (INV-RING R)
                             (INTEGERP N))
                        (EQUAL (NEW-D-TOP N (NEW-EXTERNAL-TOP N R A))
                               (NEW-EXTERNAL-TOP (+ N -1)
                                                 R (NEW-D-TOP N A))))
               (IMPLIES (INTEGERP N)
                        (EQUAL (NEW-D-TOP N (NEW-ZERO-TOP N))
                               (NEW-ZERO-TOP (+ N -1))))
               (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
                        (EQUAL (NEW-D-TOP N (NEW-INVERSE-TOP N A))
                               (NEW-INVERSE-TOP (+ N -1)
                                                (NEW-D-TOP N A)))))
          (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
                   (EQUAL (NEW-D-TOP (1- N) (NEW-D-TOP N A))
                          (NEW-ZERO-TOP (1- (1- N)))))))
    (AND
     (AND
      (AND
       (AND
           (AND (AND (IMPLIES (AND (INV-RING X) (INV-RING Y))
                              (INV-RING (ADDITION-RING X Y)))
                     (IMPLIES (AND (INV-RING X)
                                   (INV-RING Y)
                                   (INV-RING Z))
                              (EQUAL (ADDITION-RING (ADDITION-RING X Y) Z)
                                     (ADDITION-RING X (ADDITION-RING Y Z)))))
                (IMPLIES (INV-RING X)
                         (EQUAL (ADDITION-RING (ZERO-ELEMENT) X)
                                X))
                (IMPLIES (INV-RING X)
                         (EQUAL (ADDITION-RING X (ZERO-ELEMENT))
                                X))
                (INV-RING (ZERO-ELEMENT)))
           (IMPLIES (INV-RING X)
                    (EQUAL (ADDITION-RING (INVERSE X) X)
                           (ZERO-ELEMENT)))
           (IMPLIES (INV-RING X)
                    (EQUAL (ADDITION-RING X (INVERSE X))
                           (ZERO-ELEMENT)))
           (IMPLIES (INV-RING X)
                    (INV-RING (INVERSE X))))
       (AND (AND (IMPLIES (AND (INV-RING X) (INV-RING Y))
                          (INV-RING (PRODUCT-RING X Y)))
                 (IMPLIES (AND (INV-RING X)
                               (INV-RING Y)
                               (INV-RING Z))
                          (EQUAL (PRODUCT-RING (PRODUCT-RING X Y) Z)
                                 (PRODUCT-RING X (PRODUCT-RING Y Z)))))
            (IMPLIES (INV-RING X)
                     (EQUAL (PRODUCT-RING (UNIT) X) X))
            (IMPLIES (INV-RING X)
                     (EQUAL (PRODUCT-RING X (UNIT)) X))
            (INV-RING (UNIT)))
       (IMPLIES (AND (INV-RING X)
                     (INV-RING Y)
                     (INV-RING Z))
                (EQUAL (PRODUCT-RING X (ADDITION-RING Y Z))
                       (ADDITION-RING (PRODUCT-RING X Y)
                                      (PRODUCT-RING X Z))))
       (IMPLIES (AND (INV-RING X)
                     (INV-RING Y)
                     (INV-RING Z))
                (EQUAL (PRODUCT-RING (ADDITION-RING X Y) Z)
                       (ADDITION-RING (PRODUCT-RING X Z)
                                      (PRODUCT-RING Y Z)))))
      (IMPLIES (AND (NEW-INV-BOTTOM N A)
                    (NEW-INV-BOTTOM N B)
                    (INTEGERP N))
               (NEW-INV-BOTTOM N (NEW-GROUP-OPERATION-BOTTOM N A B)))
      (IMPLIES
       (AND (NEW-INV-BOTTOM N A)
            (NEW-INV-BOTTOM N B)
            (NEW-INV-BOTTOM N C)
            (INTEGERP N))
       (EQUAL
          (NEW-GROUP-OPERATION-BOTTOM N (NEW-GROUP-OPERATION-BOTTOM N A B)
                                      C)
          (NEW-GROUP-OPERATION-BOTTOM N
                                      A (NEW-GROUP-OPERATION-BOTTOM N B C))))
      (NEW-INV-BOTTOM N (NEW-ZERO-BOTTOM N))
      (IMPLIES (AND (NEW-INV-BOTTOM N A)
                    (INV-RING R)
                    (INTEGERP N))
               (NEW-INV-BOTTOM N (NEW-EXTERNAL-BOTTOM N R A)))
      (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
               (EQUAL (NEW-GROUP-OPERATION-BOTTOM N A (NEW-ZERO-BOTTOM N))
                      A))
      (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
               (NEW-INV-BOTTOM N (NEW-INVERSE-BOTTOM N A)))
      (IMPLIES (AND (NEW-INV-BOTTOM N A)
                    (NEW-INV-BOTTOM N B)
                    (INTEGERP N)
                    (EQUAL (NEW-GROUP-OPERATION-BOTTOM N A B)
                           (NEW-ZERO-BOTTOM N)))
               (EQUAL (NEW-INVERSE-BOTTOM N A) B))
      (IMPLIES
           (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
           (EQUAL (NEW-GROUP-OPERATION-BOTTOM N A (NEW-INVERSE-BOTTOM N A))
                  (NEW-ZERO-BOTTOM N)))
      (IMPLIES (AND (NEW-INV-BOTTOM N A)
                    (NEW-INV-BOTTOM N B)
                    (INTEGERP N))
               (EQUAL (NEW-GROUP-OPERATION-BOTTOM N A B)
                      (NEW-GROUP-OPERATION-BOTTOM N B A)))
      (IMPLIES
          (AND (NEW-INV-BOTTOM N A)
               (NEW-INV-BOTTOM N B)
               (INV-RING R)
               (INTEGERP N))
          (EQUAL (NEW-EXTERNAL-BOTTOM N R (NEW-GROUP-OPERATION-BOTTOM N A B))
                 (NEW-GROUP-OPERATION-BOTTOM N (NEW-EXTERNAL-BOTTOM N R A)
                                             (NEW-EXTERNAL-BOTTOM N R B))))
      (IMPLIES
           (AND (NEW-INV-BOTTOM N A)
                (INV-RING S)
                (INV-RING R)
                (INTEGERP N))
           (EQUAL (NEW-EXTERNAL-BOTTOM N (ADDITION-RING S R)
                                       A)
                  (NEW-GROUP-OPERATION-BOTTOM N (NEW-EXTERNAL-BOTTOM N S A)
                                              (NEW-EXTERNAL-BOTTOM N R A))))
      (IMPLIES (AND (NEW-INV-BOTTOM N A)
                    (INV-RING S)
                    (INV-RING R)
                    (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-BOTTOM N (PRODUCT-RING S R)
                                           A)
                      (NEW-EXTERNAL-BOTTOM N S (NEW-EXTERNAL-BOTTOM N R A))))
      (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-BOTTOM N (UNIT) A)
                      A))
      (IMPLIES
           (AND (NEW-INV-BOTTOM N A)
                (NEW-INV-BOTTOM N B)
                (INTEGERP N))
           (EQUAL (NEW-INVERSE-BOTTOM N (NEW-GROUP-OPERATION-BOTTOM N A B))
                  (NEW-GROUP-OPERATION-BOTTOM N (NEW-INVERSE-BOTTOM N A)
                                              (NEW-INVERSE-BOTTOM N B))))
      (IMPLIES (AND (NEW-INV-BOTTOM N A)
                    (INV-RING S)
                    (INTEGERP N))
               (EQUAL (NEW-INVERSE-BOTTOM N (NEW-EXTERNAL-BOTTOM N S A))
                      (NEW-EXTERNAL-BOTTOM N S (NEW-INVERSE-BOTTOM N A))))
      (IMPLIES (INTEGERP N)
               (EQUAL (NEW-INVERSE-BOTTOM N (NEW-ZERO-BOTTOM N))
                      (NEW-ZERO-BOTTOM N)))
      (IMPLIES (AND (INV-RING S) (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-BOTTOM N S (NEW-ZERO-BOTTOM N))
                      (NEW-ZERO-BOTTOM N))))
     (AND
      (AND
          (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
                   (NEW-INV-BOTTOM (+ N -1)
                                   (NEW-D-BOTTOM N A)))
          (IMPLIES (AND (NEW-INV-BOTTOM N A)
                        (NEW-INV-BOTTOM N B)
                        (INTEGERP N))
                   (EQUAL (NEW-D-BOTTOM N (NEW-GROUP-OPERATION-BOTTOM N A B))
                          (NEW-GROUP-OPERATION-BOTTOM (+ N -1)
                                                      (NEW-D-BOTTOM N A)
                                                      (NEW-D-BOTTOM N B))))
          (IMPLIES (AND (NEW-INV-BOTTOM N A)
                        (INV-RING R)
                        (INTEGERP N))
                   (EQUAL (NEW-D-BOTTOM N (NEW-EXTERNAL-BOTTOM N R A))
                          (NEW-EXTERNAL-BOTTOM (+ N -1)
                                               R (NEW-D-BOTTOM N A))))
          (IMPLIES (INTEGERP N)
                   (EQUAL (NEW-D-BOTTOM N (NEW-ZERO-BOTTOM N))
                          (NEW-ZERO-BOTTOM (+ N -1))))
          (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
                   (EQUAL (NEW-D-BOTTOM N (NEW-INVERSE-BOTTOM N A))
                          (NEW-INVERSE-BOTTOM (+ N -1)
                                              (NEW-D-BOTTOM N A)))))
      (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
               (EQUAL (NEW-D-BOTTOM (1- N) (NEW-D-BOTTOM N A))
                      (NEW-ZERO-BOTTOM (1- (1- N)))))))
    (AND (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
                  (NEW-INV-BOTTOM N (NEW-F N A)))
         (IMPLIES (AND (NEW-INV-TOP N A)
                       (NEW-INV-TOP N B)
                       (INTEGERP N))
                  (EQUAL (NEW-F N (NEW-GROUP-OPERATION-TOP N A B))
                         (NEW-GROUP-OPERATION-BOTTOM N (NEW-F N A)
                                                     (NEW-F N B))))
         (IMPLIES (AND (NEW-INV-TOP N A)
                       (INV-RING R)
                       (INTEGERP N))
                  (EQUAL (NEW-F N (NEW-EXTERNAL-TOP N R A))
                         (NEW-EXTERNAL-BOTTOM N R (NEW-F N A))))
         (IMPLIES (INTEGERP N)
                  (EQUAL (NEW-F N (NEW-ZERO-TOP N))
                         (NEW-ZERO-BOTTOM N)))
         (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
                  (EQUAL (NEW-F N (NEW-INVERSE-TOP N A))
                         (NEW-INVERSE-BOTTOM N (NEW-F N A)))))
    (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
             (EQUAL (NEW-D-BOTTOM N (NEW-F N A))
                    (NEW-F (1- N) (NEW-D-TOP N A)))))
   (AND (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
                 (NEW-INV-TOP (+ N 1) (NEW-H N A)))
        (IMPLIES (AND (NEW-INV-TOP N A)
                      (NEW-INV-TOP N B)
                      (INTEGERP N))
                 (EQUAL (NEW-H N (NEW-GROUP-OPERATION-TOP N A B))
                        (NEW-GROUP-OPERATION-TOP (+ N 1)
                                                 (NEW-H N A)
                                                 (NEW-H N B))))
        (IMPLIES (AND (NEW-INV-TOP N A)
                      (INV-RING R)
                      (INTEGERP N))
                 (EQUAL (NEW-H N (NEW-EXTERNAL-TOP N R A))
                        (NEW-EXTERNAL-TOP (+ N 1)
                                          R (NEW-H N A))))
        (IMPLIES (INTEGERP N)
                 (EQUAL (NEW-H N (NEW-ZERO-TOP N))
                        (NEW-ZERO-TOP (+ N 1))))
        (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
                 (EQUAL (NEW-H N (NEW-INVERSE-TOP N A))
                        (NEW-INVERSE-TOP (+ N 1) (NEW-H N A)))))
   (AND
    (AND
     (AND
      (AND
       (AND
           (AND (AND (IMPLIES (AND (INV-RING X) (INV-RING Y))
                              (INV-RING (ADDITION-RING X Y)))
                     (IMPLIES (AND (INV-RING X)
                                   (INV-RING Y)
                                   (INV-RING Z))
                              (EQUAL (ADDITION-RING (ADDITION-RING X Y) Z)
                                     (ADDITION-RING X (ADDITION-RING Y Z)))))
                (IMPLIES (INV-RING X)
                         (EQUAL (ADDITION-RING (ZERO-ELEMENT) X)
                                X))
                (IMPLIES (INV-RING X)
                         (EQUAL (ADDITION-RING X (ZERO-ELEMENT))
                                X))
                (INV-RING (ZERO-ELEMENT)))
           (IMPLIES (INV-RING X)
                    (EQUAL (ADDITION-RING (INVERSE X) X)
                           (ZERO-ELEMENT)))
           (IMPLIES (INV-RING X)
                    (EQUAL (ADDITION-RING X (INVERSE X))
                           (ZERO-ELEMENT)))
           (IMPLIES (INV-RING X)
                    (INV-RING (INVERSE X))))
       (AND (AND (IMPLIES (AND (INV-RING X) (INV-RING Y))
                          (INV-RING (PRODUCT-RING X Y)))
                 (IMPLIES (AND (INV-RING X)
                               (INV-RING Y)
                               (INV-RING Z))
                          (EQUAL (PRODUCT-RING (PRODUCT-RING X Y) Z)
                                 (PRODUCT-RING X (PRODUCT-RING Y Z)))))
            (IMPLIES (INV-RING X)
                     (EQUAL (PRODUCT-RING (UNIT) X) X))
            (IMPLIES (INV-RING X)
                     (EQUAL (PRODUCT-RING X (UNIT)) X))
            (INV-RING (UNIT)))
       (IMPLIES (AND (INV-RING X)
                     (INV-RING Y)
                     (INV-RING Z))
                (EQUAL (PRODUCT-RING X (ADDITION-RING Y Z))
                       (ADDITION-RING (PRODUCT-RING X Y)
                                      (PRODUCT-RING X Z))))
       (IMPLIES (AND (INV-RING X)
                     (INV-RING Y)
                     (INV-RING Z))
                (EQUAL (PRODUCT-RING (ADDITION-RING X Y) Z)
                       (ADDITION-RING (PRODUCT-RING X Z)
                                      (PRODUCT-RING Y Z)))))
      (IMPLIES (AND (NEW-INV-BOTTOM N A)
                    (NEW-INV-BOTTOM N B)
                    (INTEGERP N))
               (NEW-INV-BOTTOM N (NEW-GROUP-OPERATION-BOTTOM N A B)))
      (IMPLIES
       (AND (NEW-INV-BOTTOM N A)
            (NEW-INV-BOTTOM N B)
            (NEW-INV-BOTTOM N C)
            (INTEGERP N))
       (EQUAL
          (NEW-GROUP-OPERATION-BOTTOM N (NEW-GROUP-OPERATION-BOTTOM N A B)
                                      C)
          (NEW-GROUP-OPERATION-BOTTOM N
                                      A (NEW-GROUP-OPERATION-BOTTOM N B C))))
      (NEW-INV-BOTTOM N (NEW-ZERO-BOTTOM N))
      (IMPLIES (AND (NEW-INV-BOTTOM N A)
                    (INV-RING R)
                    (INTEGERP N))
               (NEW-INV-BOTTOM N (NEW-EXTERNAL-BOTTOM N R A)))
      (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
               (EQUAL (NEW-GROUP-OPERATION-BOTTOM N A (NEW-ZERO-BOTTOM N))
                      A))
      (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
               (NEW-INV-BOTTOM N (NEW-INVERSE-BOTTOM N A)))
      (IMPLIES (AND (NEW-INV-BOTTOM N A)
                    (NEW-INV-BOTTOM N B)
                    (INTEGERP N)
                    (EQUAL (NEW-GROUP-OPERATION-BOTTOM N A B)
                           (NEW-ZERO-BOTTOM N)))
               (EQUAL (NEW-INVERSE-BOTTOM N A) B))
      (IMPLIES
           (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
           (EQUAL (NEW-GROUP-OPERATION-BOTTOM N A (NEW-INVERSE-BOTTOM N A))
                  (NEW-ZERO-BOTTOM N)))
      (IMPLIES (AND (NEW-INV-BOTTOM N A)
                    (NEW-INV-BOTTOM N B)
                    (INTEGERP N))
               (EQUAL (NEW-GROUP-OPERATION-BOTTOM N A B)
                      (NEW-GROUP-OPERATION-BOTTOM N B A)))
      (IMPLIES
          (AND (NEW-INV-BOTTOM N A)
               (NEW-INV-BOTTOM N B)
               (INV-RING R)
               (INTEGERP N))
          (EQUAL (NEW-EXTERNAL-BOTTOM N R (NEW-GROUP-OPERATION-BOTTOM N A B))
                 (NEW-GROUP-OPERATION-BOTTOM N (NEW-EXTERNAL-BOTTOM N R A)
                                             (NEW-EXTERNAL-BOTTOM N R B))))
      (IMPLIES
           (AND (NEW-INV-BOTTOM N A)
                (INV-RING S)
                (INV-RING R)
                (INTEGERP N))
           (EQUAL (NEW-EXTERNAL-BOTTOM N (ADDITION-RING S R)
                                       A)
                  (NEW-GROUP-OPERATION-BOTTOM N (NEW-EXTERNAL-BOTTOM N S A)
                                              (NEW-EXTERNAL-BOTTOM N R A))))
      (IMPLIES (AND (NEW-INV-BOTTOM N A)
                    (INV-RING S)
                    (INV-RING R)
                    (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-BOTTOM N (PRODUCT-RING S R)
                                           A)
                      (NEW-EXTERNAL-BOTTOM N S (NEW-EXTERNAL-BOTTOM N R A))))
      (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-BOTTOM N (UNIT) A)
                      A))
      (IMPLIES
           (AND (NEW-INV-BOTTOM N A)
                (NEW-INV-BOTTOM N B)
                (INTEGERP N))
           (EQUAL (NEW-INVERSE-BOTTOM N (NEW-GROUP-OPERATION-BOTTOM N A B))
                  (NEW-GROUP-OPERATION-BOTTOM N (NEW-INVERSE-BOTTOM N A)
                                              (NEW-INVERSE-BOTTOM N B))))
      (IMPLIES (AND (NEW-INV-BOTTOM N A)
                    (INV-RING S)
                    (INTEGERP N))
               (EQUAL (NEW-INVERSE-BOTTOM N (NEW-EXTERNAL-BOTTOM N S A))
                      (NEW-EXTERNAL-BOTTOM N S (NEW-INVERSE-BOTTOM N A))))
      (IMPLIES (INTEGERP N)
               (EQUAL (NEW-INVERSE-BOTTOM N (NEW-ZERO-BOTTOM N))
                      (NEW-ZERO-BOTTOM N)))
      (IMPLIES (AND (INV-RING S) (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-BOTTOM N S (NEW-ZERO-BOTTOM N))
                      (NEW-ZERO-BOTTOM N))))
     (AND
      (AND
          (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
                   (NEW-INV-BOTTOM (+ N -1)
                                   (NEW-D-BOTTOM N A)))
          (IMPLIES (AND (NEW-INV-BOTTOM N A)
                        (NEW-INV-BOTTOM N B)
                        (INTEGERP N))
                   (EQUAL (NEW-D-BOTTOM N (NEW-GROUP-OPERATION-BOTTOM N A B))
                          (NEW-GROUP-OPERATION-BOTTOM (+ N -1)
                                                      (NEW-D-BOTTOM N A)
                                                      (NEW-D-BOTTOM N B))))
          (IMPLIES (AND (NEW-INV-BOTTOM N A)
                        (INV-RING R)
                        (INTEGERP N))
                   (EQUAL (NEW-D-BOTTOM N (NEW-EXTERNAL-BOTTOM N R A))
                          (NEW-EXTERNAL-BOTTOM (+ N -1)
                                               R (NEW-D-BOTTOM N A))))
          (IMPLIES (INTEGERP N)
                   (EQUAL (NEW-D-BOTTOM N (NEW-ZERO-BOTTOM N))
                          (NEW-ZERO-BOTTOM (+ N -1))))
          (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
                   (EQUAL (NEW-D-BOTTOM N (NEW-INVERSE-BOTTOM N A))
                          (NEW-INVERSE-BOTTOM (+ N -1)
                                              (NEW-D-BOTTOM N A)))))
      (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
               (EQUAL (NEW-D-BOTTOM (1- N) (NEW-D-BOTTOM N A))
                      (NEW-ZERO-BOTTOM (1- (1- N)))))))
    (AND
     (AND
      (AND
       (AND
           (AND (AND (IMPLIES (AND (INV-RING X) (INV-RING Y))
                              (INV-RING (ADDITION-RING X Y)))
                     (IMPLIES (AND (INV-RING X)
                                   (INV-RING Y)
                                   (INV-RING Z))
                              (EQUAL (ADDITION-RING (ADDITION-RING X Y) Z)
                                     (ADDITION-RING X (ADDITION-RING Y Z)))))
                (IMPLIES (INV-RING X)
                         (EQUAL (ADDITION-RING (ZERO-ELEMENT) X)
                                X))
                (IMPLIES (INV-RING X)
                         (EQUAL (ADDITION-RING X (ZERO-ELEMENT))
                                X))
                (INV-RING (ZERO-ELEMENT)))
           (IMPLIES (INV-RING X)
                    (EQUAL (ADDITION-RING (INVERSE X) X)
                           (ZERO-ELEMENT)))
           (IMPLIES (INV-RING X)
                    (EQUAL (ADDITION-RING X (INVERSE X))
                           (ZERO-ELEMENT)))
           (IMPLIES (INV-RING X)
                    (INV-RING (INVERSE X))))
       (AND (AND (IMPLIES (AND (INV-RING X) (INV-RING Y))
                          (INV-RING (PRODUCT-RING X Y)))
                 (IMPLIES (AND (INV-RING X)
                               (INV-RING Y)
                               (INV-RING Z))
                          (EQUAL (PRODUCT-RING (PRODUCT-RING X Y) Z)
                                 (PRODUCT-RING X (PRODUCT-RING Y Z)))))
            (IMPLIES (INV-RING X)
                     (EQUAL (PRODUCT-RING (UNIT) X) X))
            (IMPLIES (INV-RING X)
                     (EQUAL (PRODUCT-RING X (UNIT)) X))
            (INV-RING (UNIT)))
       (IMPLIES (AND (INV-RING X)
                     (INV-RING Y)
                     (INV-RING Z))
                (EQUAL (PRODUCT-RING X (ADDITION-RING Y Z))
                       (ADDITION-RING (PRODUCT-RING X Y)
                                      (PRODUCT-RING X Z))))
       (IMPLIES (AND (INV-RING X)
                     (INV-RING Y)
                     (INV-RING Z))
                (EQUAL (PRODUCT-RING (ADDITION-RING X Y) Z)
                       (ADDITION-RING (PRODUCT-RING X Z)
                                      (PRODUCT-RING Y Z)))))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (NEW-INV-TOP N B)
                    (INTEGERP N))
               (NEW-INV-TOP N (NEW-GROUP-OPERATION-TOP N A B)))
      (IMPLIES
       (AND (NEW-INV-TOP N A)
            (NEW-INV-TOP N B)
            (NEW-INV-TOP N C)
            (INTEGERP N))
       (EQUAL (NEW-GROUP-OPERATION-TOP N (NEW-GROUP-OPERATION-TOP N A B)
                                       C)
              (NEW-GROUP-OPERATION-TOP N A (NEW-GROUP-OPERATION-TOP N B C))))
      (NEW-INV-TOP N (NEW-ZERO-TOP N))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (INV-RING R)
                    (INTEGERP N))
               (NEW-INV-TOP N (NEW-EXTERNAL-TOP N R A)))
      (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
               (EQUAL (NEW-GROUP-OPERATION-TOP N A (NEW-ZERO-TOP N))
                      A))
      (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
               (NEW-INV-TOP N (NEW-INVERSE-TOP N A)))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (NEW-INV-TOP N B)
                    (INTEGERP N)
                    (EQUAL (NEW-GROUP-OPERATION-TOP N A B)
                           (NEW-ZERO-TOP N)))
               (EQUAL (NEW-INVERSE-TOP N A) B))
      (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
               (EQUAL (NEW-GROUP-OPERATION-TOP N A (NEW-INVERSE-TOP N A))
                      (NEW-ZERO-TOP N)))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (NEW-INV-TOP N B)
                    (INTEGERP N))
               (EQUAL (NEW-GROUP-OPERATION-TOP N A B)
                      (NEW-GROUP-OPERATION-TOP N B A)))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (NEW-INV-TOP N B)
                    (INV-RING R)
                    (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-TOP N R (NEW-GROUP-OPERATION-TOP N A B))
                      (NEW-GROUP-OPERATION-TOP N (NEW-EXTERNAL-TOP N R A)
                                               (NEW-EXTERNAL-TOP N R B))))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (INV-RING S)
                    (INV-RING R)
                    (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-TOP N (ADDITION-RING S R)
                                        A)
                      (NEW-GROUP-OPERATION-TOP N (NEW-EXTERNAL-TOP N S A)
                                               (NEW-EXTERNAL-TOP N R A))))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (INV-RING S)
                    (INV-RING R)
                    (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-TOP N (PRODUCT-RING S R)
                                        A)
                      (NEW-EXTERNAL-TOP N S (NEW-EXTERNAL-TOP N R A))))
      (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-TOP N (UNIT) A) A))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (NEW-INV-TOP N B)
                    (INTEGERP N))
               (EQUAL (NEW-INVERSE-TOP N (NEW-GROUP-OPERATION-TOP N A B))
                      (NEW-GROUP-OPERATION-TOP N (NEW-INVERSE-TOP N A)
                                               (NEW-INVERSE-TOP N B))))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (INV-RING S)
                    (INTEGERP N))
               (EQUAL (NEW-INVERSE-TOP N (NEW-EXTERNAL-TOP N S A))
                      (NEW-EXTERNAL-TOP N S (NEW-INVERSE-TOP N A))))
      (IMPLIES (INTEGERP N)
               (EQUAL (NEW-INVERSE-TOP N (NEW-ZERO-TOP N))
                      (NEW-ZERO-TOP N)))
      (IMPLIES (AND (INV-RING S) (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-TOP N S (NEW-ZERO-TOP N))
                      (NEW-ZERO-TOP N))))
     (AND (AND (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
                        (NEW-INV-TOP (+ N -1) (NEW-D-TOP N A)))
               (IMPLIES (AND (NEW-INV-TOP N A)
                             (NEW-INV-TOP N B)
                             (INTEGERP N))
                        (EQUAL (NEW-D-TOP N (NEW-GROUP-OPERATION-TOP N A B))
                               (NEW-GROUP-OPERATION-TOP (+ N -1)
                                                        (NEW-D-TOP N A)
                                                        (NEW-D-TOP N B))))
               (IMPLIES (AND (NEW-INV-TOP N A)
                             (INV-RING R)
                             (INTEGERP N))
                        (EQUAL (NEW-D-TOP N (NEW-EXTERNAL-TOP N R A))
                               (NEW-EXTERNAL-TOP (+ N -1)
                                                 R (NEW-D-TOP N A))))
               (IMPLIES (INTEGERP N)
                        (EQUAL (NEW-D-TOP N (NEW-ZERO-TOP N))
                               (NEW-ZERO-TOP (+ N -1))))
               (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
                        (EQUAL (NEW-D-TOP N (NEW-INVERSE-TOP N A))
                               (NEW-INVERSE-TOP (+ N -1)
                                                (NEW-D-TOP N A)))))
          (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
                   (EQUAL (NEW-D-TOP (1- N) (NEW-D-TOP N A))
                          (NEW-ZERO-TOP (1- (1- N)))))))
    (AND (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
                  (NEW-INV-TOP N (NEW-G N A)))
         (IMPLIES (AND (NEW-INV-BOTTOM N A)
                       (NEW-INV-BOTTOM N B)
                       (INTEGERP N))
                  (EQUAL (NEW-G N (NEW-GROUP-OPERATION-BOTTOM N A B))
                         (NEW-GROUP-OPERATION-TOP N (NEW-G N A)
                                                  (NEW-G N B))))
         (IMPLIES (AND (NEW-INV-BOTTOM N A)
                       (INV-RING R)
                       (INTEGERP N))
                  (EQUAL (NEW-G N (NEW-EXTERNAL-BOTTOM N R A))
                         (NEW-EXTERNAL-TOP N R (NEW-G N A))))
         (IMPLIES (INTEGERP N)
                  (EQUAL (NEW-G N (NEW-ZERO-BOTTOM N))
                         (NEW-ZERO-TOP N)))
         (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
                  (EQUAL (NEW-G N (NEW-INVERSE-BOTTOM N A))
                         (NEW-INVERSE-TOP N (NEW-G N A)))))
    (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
             (EQUAL (NEW-D-TOP N (NEW-G N A))
                    (NEW-G (1- N) (NEW-D-BOTTOM N A)))))
   (IMPLIES (AND (NEW-INV-BOTTOM N GNRT)
                 (INTEGERP N))
            (EQUAL (NEW-F N (NEW-G N GNRT)) GNRT))
   (IMPLIES
    (AND (NEW-INV-TOP N GNRT) (INTEGERP N))
    (EQUAL
     (NEW-GROUP-OPERATION-TOP N (NEW-H (1- N) (NEW-D-TOP N GNRT))
                              (NEW-D-TOP (1+ N) (NEW-H N GNRT)))
     (NEW-GROUP-OPERATION-TOP N GNRT
                              (NEW-INVERSE-TOP N (NEW-G N (NEW-F N GNRT))))))
   (IMPLIES (AND (NEW-INV-TOP N GNRT) (INTEGERP N))
            (EQUAL (NEW-F (1+ N) (NEW-H N GNRT))
                   (NEW-ZERO-BOTTOM (1+ N))))
   (IMPLIES (AND (NEW-INV-BOTTOM N GNRT)
                 (INTEGERP N))
            (EQUAL (NEW-H N (NEW-G N GNRT))
                   (NEW-ZERO-TOP (1+ N))))
   (IMPLIES (AND (NEW-INV-TOP N GNRT) (INTEGERP N))
            (EQUAL (NEW-H (1+ N) (NEW-H N GNRT))
                   (NEW-ZERO-TOP (1+ (1+ N))))))
  :HINTS (("Subgoal 45" :USE ((:INSTANCE NEW-D-D-TOP)))
          ("Subgoal 23" :USE ((:INSTANCE PERTURBATIONOPERTURBATION))))))
)


(make-generic-theory *tpl*)